(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
subtrees(@t) → subtrees#1(@t)
subtrees#1(leaf) → nil
subtrees#1(node(@x, @t1, @t2)) → subtrees#2(subtrees(@t1), @t1, @t2, @x)
subtrees#2(@l1, @t1, @t2, @x) → subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
subtrees#3(@l2, @l1, @t1, @t2, @x) → ::(node(@x, @t1, @t2), append(@l1, @l2))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to relative TRS where S is empty.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
subtrees(@t) → subtrees#1(@t)
subtrees#1(leaf) → nil
subtrees#1(node(@x, @t1, @t2)) → subtrees#2(subtrees(@t1), @t1, @t2, @x)
subtrees#2(@l1, @t1, @t2, @x) → subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
subtrees#3(@l2, @l1, @t1, @t2, @x) → ::(node(@x, @t1, @t2), append(@l1, @l2))
S is empty.
Rewrite Strategy: INNERMOST
(3) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
::/0
node/0
subtrees#2/1
subtrees#2/3
subtrees#3/2
subtrees#3/3
subtrees#3/4
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@xs), @l2) → ::(append(@xs, @l2))
append#1(nil, @l2) → @l2
subtrees(@t) → subtrees#1(@t)
subtrees#1(leaf) → nil
subtrees#1(node(@t1, @t2)) → subtrees#2(subtrees(@t1), @t2)
subtrees#2(@l1, @t2) → subtrees#3(subtrees(@t2), @l1)
subtrees#3(@l2, @l1) → ::(append(@l1, @l2))
S is empty.
Rewrite Strategy: INNERMOST
(5) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
append(::(@xs3_0), @l2) →+ ::(append(@xs3_0, @l2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [@xs3_0 / ::(@xs3_0)].
The result substitution is [ ].
(6) BOUNDS(n^1, INF)